package flowlogic;

import java.util.ArrayList;
import java.util.HashMap;
import java.util.HashSet;
import java.util.LinkedList;

import ast.DQCSystem;
import ast.Term;

import com.microsoft.z3.Context;
import com.microsoft.z3.Solver;
import com.microsoft.z3.Z3Exception;

public class FLAnalysis {
	
	private static Context ctx;
	private static Solver solver;
	private static HashMap<String, HashSet<Term>> rho;
	private static HashMap<String, HashSet<Term>> kappa;
	private static PsiNode psi;
	
	
	private static ArrayList<Constraint> constraintList = 
			new ArrayList<Constraint>();

	public static void init()
	{
		HashMap<String, String> cfg = new HashMap<String, String>();
        cfg.put("model", "true");
        try {
			ctx = new Context(cfg);
			solver = ctx.mkSolver();
		} catch (Z3Exception e) {
			// TODO Auto-generated catch block
			e.printStackTrace();
		}
        
        constraintList.clear();
	}
	
	public static void unfold(DQCSystem sys)
	{
//		System.out.println("\nThe unfolding process:");
		
		LinkedList<FLJudgement> judgementList = new LinkedList<FLJudgement>();
		SystemJudgement sysjdgt = new SystemJudgement(sys);
		rho = sysjdgt.getRho();
		kappa = sysjdgt.getKappa();
		psi = sysjdgt.getPsi();
		
		judgementList.add(sysjdgt);
		while (!judgementList.isEmpty()) {
			FLJudgement curJdgt = judgementList.removeFirst();
			ArrayList<DischargeResult> dischargeRes = null;
			try {
				dischargeRes = curJdgt.discharge();
			} catch (Z3Exception e) {
				// TODO Auto-generated catch block
				e.printStackTrace();
			}
			
			for (DischargeResult curRes : dischargeRes) {
				if (curRes instanceof FLJudgement) {
					judgementList.addLast((FLJudgement) curRes);
				} else {
					constraintList.add((Constraint) curRes);
				}
			}
			
//			System.out.println("\nFrom " + curJdgt);
//			System.out.println("To");
//			for (DischargeResult dr : dischargeRes) {
//				System.out.println(dr);
//			}
		}
	}
	
	public static void solve()
	{
		boolean changed;
		
//		System.out.println("\n\nThe constraint solving process:\n");
		
		do {
			changed = false;
			
			boolean hld;
			for (Constraint cs : constraintList) {
				
				ConstraintSolver flSolver = new ConstraintSolver(rho, kappa);
				hld = flSolver.solve(cs);
				if (!hld) {
					changed = true;
				}
				
			}
			
//			System.out.println("\n\nThe result for rho:\n");
//			for (String nm : rho.keySet()) {
//				System.out.println(nm + "->" + rho.get(nm));
//			}
			
//			System.out.println("\n\nThe result for kappa:\n\n");
//			for (String nm : kappa.keySet()) {
//				System.out.println(nm + "->" + kappa.get(nm));
//			}
//			System.out.println();
			
		} while (changed);
		
	}
	
	public static void cleanup()
	{
		ctx.dispose();
	}
	
	public static Solver getSolver()
	{
		return solver;
	}
	
	public static Context getCtx()
	{
		return ctx;
	}

	public static ArrayList<Constraint> getConstraintList() {
		return constraintList;
	}

	public static HashMap<String, HashSet<Term>> getRho() {
		return rho;
	}
	
	public static PsiNode getPsi()
	{
		return psi;
	}
	
}
